1. $T$ : Type
\\[0ex]2. $L$ : $T$ List
\\[0ex]3. $x$ : $T$
\\[0ex]4. $y$ : $T$
\\[0ex]5. $i$ : \{0..($\parallel$$L$$\parallel$ {-} 1)$^{-}$\}
\\[0ex]6. $x$ = $L$[$i$]
\\[0ex]7. $y$ = $L$[($i$+1)]
\\[0ex]$\vdash$  $\exists$$f$:\{0..2$^{-}$\}$\rightarrow$\{0..$\parallel$$L$$\parallel^{-}$\}. (increasing($f$;2) \& ($\forall$$j$:\{0..2$^{-}$\}. [$x$; $y$][$j$] = $L$[($f$($j$))]))